%% RiSE Latex Template - version 0.5
%%
%% RiSE's latex template for thesis and dissertations
%% http://risetemplate.sourceforge.net
%%
%% (c) 2010 Yguaratã Cerqueira Cavalcanti (yguarata@gmail.com)
%%          Vinicius Cardoso Garcia (vinicius.garcia@gmail.com)
%%
%% This document was initially based on UFPEThesis template, from Paulo Gustavo
%% S. Fonseca.
%%
%% ACKNOWLEDGEMENTS
%%
%% We would like to thanks the RiSE's researchers community, the 
%% students from Federal University of Pernambuco, and other users that have
%% been contributing to this projects with comments and patches.
%%
%% GENERAL INSTRUCTIONS
%%
%% We strongly recommend you to compile your documents using pdflatex command.
%% It is also recommend use the texlipse plugin for Eclipse to edit your documents.
%%
%% Options:
%%         * Idiom
%%           pt   - Portguese (default)
%%           en   - English
%%
%%         * Text type
%%           bsc  - B.Sc. Thesis
%%           msc  - M.Sc. Thesis (default)
%%           qual - PHD qualification (not tested yet)
%%           prop - PHD proposal (not tested yet)
%%           phd  - PHD thesis
%%
%%         * Media
%%           scr  - to eletronic version (PDF) / see the users guide
%%
%%         * Pagination
%%           oneside - unique face press
%%           twoside - two faces press
%%
%%		   * Line spacing
%%           singlespacing  - the same as using \linespread{1}
%%           onehalfspacing - the same as using \linespread{1.3}
%%           doublespacing  - the same as using \linespread{1.6}
%%
%% Reference commands. Use the following commands to make references in your
%% text:
%%          \figref  -- for Figure reference
%%          \tabref  -- for Table reference
%%          \eqnref  -- for equation reference
%%          \chapref -- for chapter reference
%%          \secref  -- for section reference
%%          \appref  -- for appendix reference
%%          \axiref  -- for axiom reference
%%          \conjref -- for conjecture reference
%%          \defref  -- for definition reference
%%          \lemref  -- for lemma reference
%%          \theoref -- for theorem reference
%%          \corref  -- for corollary reference
%%          \propref -- for proprosition reference
%%          \pgref   -- for page reference
%%
%%          Example: See \chapref{chap:introduction}. It will produce 
%%                   'See Chapter 1', in case of English language.
\documentclass[en,oneside,onehalfspacing]{risethesis}

\usepackage[numbers]{natbib}
\usepackage{babel}
\usepackage{supertabular}
\usepackage{fancybox}
\usepackage{acronym}
%% Change the following pdf author attribute name to your name.
\usepackage[linkcolor=blue,citecolor=blue,urlcolor=blue,colorlinks,pdfpagelabels,pdftitle={jpso-msc},pdfauthor={Joao Paulo Oliveira}]{hyperref}

\usepackage{array}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{hhline}
\usepackage{epsfig}
\usepackage{listings}
\usepackage{subfigure}
\usepackage[table]{xcolor}
\usepackage{color}
\usepackage{epic,eepic}
\usepackage{url}
\usepackage{cite}
\usepackage{multirow}
\usepackage{graphicx}
\usepackage{wrapfig}
\usepackage{lmodern}
%\usepackage{landscape}
\usepackage{rotating}
\address{Recife}

\universitypt{Universidade Federal de Pernambuco}
\universityen{Federal University of Pernambuco}

\departmentpt{Centro de Informática}
\departmenten{Center for Informatics}

\programpt{Pós-graduação em Ciência da Computação}
\programen{Graduate in Computer Science}

\majorfieldpt{Ciência da Computação}
\majorfielden{Computer Science}

\input{macros}

\title{\tname{}: A novel approach to find data-races during state-space
exploration}
\date{August/2012}

\author{Jo\~{a}o Paulo dos Santos Oliveira}
\adviser{Fernando Jos\'{e} Castor de Lima Filho}
\coadviser{Marcelo Bezerra d'Amorim}

\begin{document}

\frontmatter
\frontpage
\presentationpage


\renewcommand{\abstrname}{Resumo}
\begin{abstract}

\end{abstract}

%%%%%%%%%%%%%%%%%%%%%% our macros
\begin{abstract}
Data-races are an important kind of error in concurrent shared-memory
programs.\Comment{ Finding these errors remains a challenging task.}
Software model checking is a popular approach to find them\Comment{:
  it explores the state-space of a program reachable from an informed
  test driver in seek of errors.  Unfortunately, the approach can be
  very expensive for scenarios that produce very large state-spaces}.
This paper proposes a novel approach to find races that
\emph{complements} model-checking by efficiently reporting precise
\emph{warnings} during state-space exploration (SSE): \tname{}.  It
uses information obtained across different paths explored during SSE
to \emph{predict} likely racy memory accesses.  \Comment{It builds on
  the observation that, during SSE, memory accesses are covered much
  sooner than the actual race and that it is possible to relate object
  ids across exploration.}  We evaluated \tname{} on \numCases{}
different scenarios of race, involving a total of \numSubjects{}
distinct application subjects of various sources and sizes.  Results
indicate that \tname{} reports race warnings very soon compared to the
time the model checker detects the race (for \perGoodCases{} of the
cases it reports a true warning of race in $<$5s) and that the
warnings it reports include very few false alarms\Comment{, and that
  the overhead on overall exploration time is, on average, low.}.  We
also observed that the model checker finds the actual race quickly
when it uses a guided-search that builds on \tname{}'s output (for
74.2\% of the cases it reports the race in $<$20s).
\end{abstract}


\begin{dedicatory}
To my father and my mother.
\end{dedicatory}
 
 
\renewcommand{\abstrname}{Acknowledgements}
\begin{abstract}
This research would not have been possible without the support of many. Firstly,
I would like to thank my coadvisor, Marcelo d'Amorim. I owe Marcelo for his
patience and guidance. I started to work with Marcelo in January 2011 after take
some class with him. Marcelo helped me focus on a the research that lead
to this dissertation, beyond that, Marcelo motivated me in several times I
was discouraged during this work.
I want to thank you to my advisor Fernando Castor. Castor is an exceptional
professor and with its enthusiasm made me interested in concurrent programming.
I also would like to thank you to all of my friends of software engineering
laboratory that helped me in my research, especially to Benito, Weslley e Elton.
I want to thank specially the members of my dissertation committee, the
professor Roberta Coelho and Alexandre Mota to accepted that invitation and help
to improve my work.


\end{abstract}


%\begin{IEEEkeywords}
%~testing; software model checking; warnings.
%\end{IEEEkeywords}

%\maketitle              % typeset the title of the contribution
\tableofcontents
\listoffigures
\listoftables
% Acronyms
%\input{acronyms}

\mainmatter
\include{chapters/intro/intro}
\include{chapters/background/background}
\include{chapters/approach/example}
\include{chapters/approach/approach}
\include{chapters/eval/eval-new}
%\include{chapters/schedule/schedule}
%\input{related}
\include{chapters/conclusion/conclusions}


% ---- Bibliography ----


\bibliographystyle{plain} 
\bibliography{testing}

\end{document}

